T:Type, R:(TT), x, y:T. (x (R^*) y)  ((z:T. ((x R z) & (z (R^*) y)))  (x = y)) 

latex

Definitions	R^*, P  Q, P  Q, P  Q, , x f y, f(a), rel_exp(T;R;n), x:A. B(x), s = t, x:AB(x), , t  T, Type, P  Q, left + right, P & Q, x:A. B(x), x:A  B(x), A c B, n - m, #$n, , {x:A| B(x)} , A, False, Void, a < b, n+m, -n, A  B, {T}, T, True, (i = j)
Lemmas	true wf, squash wf, le wf, rel exp iff2, rel exp wf, nat wf